/*!
 * \file iegenlib_context.h
 *
 * \brief Declaration of the IEGenLib context class.
 *
 * The IEGenLibContext class represents a global context used in IEGenLib.
 * This includes information such as global settings, symbolic constants,
 * inverse function pairs, etc.
 *
 * Copyright (c) 2010, Colorado State University <br>
 * All rights reserved. <br>
 * See ../../COPYING for details. <br>
 *
 * \date Started: 12/20/10
 * \date Last Modified: 12/20/10
 * \authors Alan LaMielle
 */

#ifndef IEGENLIB_CONTEXT_H_
#define IEGENLIB_CONTEXT_H_

#include <iegenlib/iegenlib.h>
#include <set>
#include <map>

using std::set;
using std::pair;
using std::map;

namespace iegenlib{

/*!
 * \class IEGenLibContext
 *
 * \brief A global context used to define symbolic constants, uninterpreted
 * function symbols and their inverses, and other global settings used by
 * IEGenLib.
 */
class IEGenLibContext {
public:

  /*!
   * IEGenLibContext constructor
   */
  IEGenLibContext(bool simplifyConjunctions=true);

  /*!
   * IEGenLibContext equality operator
   */
  bool operator==(IEGenLibContext const& other) const;

  /*!
   * IEGenLibContext not equals operator
   */
  inline bool operator!=(IEGenLibContext const& other) const{
     return !(*this==other);}

  /*!
   * Simplify conjunctions getter.  This field defines whether or not
   * conjunctions will be simplified after constructing a set or relation and
   * after operations.
   *
   * @return true if conjunctions will be simplified, false if otherwise
   */
  inline bool getSimplifyConjunctions() const {return this->simplifyConjunctions;}

  /*!
   * Simplify conjunctions setter.  This field defines whether or not
   * conjunctions will be simplified after constructing a set or relation and
   * after operations.
   *
   * @param val true if conjunctions should be simplified, false otherwise
   */
  inline void setSimplifyConjunctions(bool val) {this->simplifyConjunctions=val;}

  /*!
   * Add the name of a symbolic constant to the context.
   */
  inline void addSymbolic(Symbolic name) {this->symbolics.insert(name);}

  /*!
   * Get the current set of symbolic constants in the context.
   *
   * @return the set of symbolic constants in the context
   */
  inline set<Symbolic> getSymbolics() const{return this->symbolics;}

  /*!
   * Get the current set of names of symbolic constants.
   *
   * @return the set of names of symbolic constants in the context
   */
  set<string> getSymbolicNames() const;

  /*!
   * Adds a pair of function names that are inverses.
   *
   * Raises a StringException if:
   * -either name is an empty string.
   * -the names are the same
   * -either name is already a know inverse
   *
   * @param name1 the first function name
   * @param name2 the second function name
   */
  void addInversePair(string name1,string name2);

  /*!
   * Get the set of pairs of inverse functions.
   *
   * @return the set of pairs of inverse functions
   */
  set<pair<string,string> > getInversePairs() const;

  /*!
   * Returns true if the given name is/has a known inverse, false otherwise.
   *
   * @param name name of the function to check for an inverse
   * @param inverse out parameter, set to the name of the inverse if found
   * @return true if an inverse if found for the given name, false otherwise
   */
  bool hasInverse(string name,string &inverse) const;

private:
  bool simplifyConjunctions;
  set<Symbolic> symbolics;

  //Mappings from function name to function name, both directions
  map<string,string> inverse_pairs1;
  map<string,string> inverse_pairs2;
};

}//end namespace iegenlib

#endif /* IEGENLIB_CONTEXT_H_ */
